ePMC

Benchmark
Model:consensus v.1 (MDP)
Parameter(s)N = 4, K = 4
Property:disagree (prob-reach)
Invocation (default)
java -Xms10240m -Xmx10240m -jar ../epmc-standard.jar check --model-input-files consensus.4.prism --model-input-type prism --property-input-files consensus.props --property-input-names disagree --translate-messages false --value-floating-point-output-native true --graphsolver-iterative-stop-criterion relative --graphsolver-iterative-tolerance 1e-6 --const K=4
Execution
Walltime:5.8837244510650635s
Return code:0
Relative Error:5.52340564152121e-05
Log
assertions-disabled
start-parsing
done-parsing
model-checking
analysing-property disagree
start-building-explorer
start-building-initial-states-explorer
done-building-initial-states-explorer
done-building-explorer
build-model-start
build-model-done 43136 0
iterating
iterating-progress-unbounded 1636 0.003157493217528379 1
iterating-progress-unbounded 3384 1.6968809149166391E-4 2
iterating-progress-unbounded 5132 8.554855640755957E-6 3
iterating-done 6741 3
model-checking-done 5
command-check-result-is 0.15606444343964274 disagree